package tr.edu.ege.kipler.test;

import tr.edu.ege.kipler.parsing.Parser;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression.Operator;
import var.syntax.BeliefOperator;

public class FLib {
	public static WorldElement cdAEqualsC() {
		return Parser
				.parseFormulaWithNs(NsUtil.getNsDef() + "mine:A = mine:C;");
	}

	public static WorldElement cdAEqualsD() {
		return Parser
				.parseFormulaWithNs(NsUtil.getNsDef() + "mine:A = mine:D;");
	}

	public static WorldElement caCx() {
		return Parser.parseFormulaWithNs(NsUtil.getNsDef() + "mine:C(mine:x);");
	}

	public static WorldElement caDy() {
		return Parser.parseFormulaWithNs(NsUtil.getNsDef() + "mine:D(mine:y);");
	}

	public static WorldElement raXValueY() {
		return Parser.parseFormulaWithNs(NsUtil.getNsDef()
				+ "mine:value(mine:x, mine:y);");
	}

	public static WorldElement iBelievesPhi(WorldElement phi) {
		return new ModalExpression(BeliefOperator.boxBelief("i"), phi);
	}

	public static WorldElement iDiaBelievesPhi(WorldElement phi) {
		return new ModalExpression(BeliefOperator.diamondBelief("i"), phi);
	}

	public static WorldElement andPhiPsi(WorldElement phi, WorldElement psi) {
		return new BinaryBooleanExpression(Operator.AND, phi, psi);
	}

	public static WorldElement orPhiPsi(WorldElement phi, WorldElement psi) {
		return new BinaryBooleanExpression(Operator.OR, phi, psi);
	}
}
